the_w:World, tg:Id, mss:Msg List. w-tagged(tg;mss)  Msg List 

latex

Definitions	World, Msg, w-tagged(tg;mss), w.M, filter(P;l), a = b, mtag(m), Msg(M), x:A. B(x), t  T, Id
Lemmas	Id wf, Msg wf, mtag wf, eq id wf, filter wf, world wf